This entry is about the theorem in logic which is often just called Diaconescu’s theorem, but not to be confused with Diaconescu's theorem in topos theory.
The Diaconescu-Goodman–Myhill theorem (Diaconescu 75, Goodman-Myhill 78) states that the law of excluded middle may be regarded as a very weak form of the axiom of choice.
The following are equivalent:
(Here, a set is finite or finitely-indexed (respectively) if, for some natural number , there is a bijection or surjection (respectively) .)
The proof is as follows. If is a truth value, then divide by the equivalence relation where iff holds. Then we have a surjection , whose domain is (and in particular, finite), and whose codomain is finitely-indexed. But this surjection splits iff is true or false, so if either is choice or -indexed sets are projective, then PEM holds.
On the other hand, if PEM holds, then we can show by induction that if and are choice, so is (add details). Thus, all finite sets are choice. Now if is a surjection, exhibiting as finitely indexed, it has a section . Since a finite set is always projective, and any retract of a projective object is projective, this shows that is projective.
In particular, the axiom of choice implies PEM. This argument, due originally to Diaconescu 75, can be internalized in any topos. However, other weak versions of choice such as countable choice (any surjection to a countable set (which for this purpose is any set isomorphic to the set of natural numbers) has a section), dependent choice, or even COSHEP do not imply PEM. In fact, it is often claimed that axiom of choice is true in constructive mathematics (by the BHK or Brouwer-Heyting-Kolmogorov interpretation of predicate logic), leading to much argument about exactly what that means.
Radu Diaconescu, Axiom of choice and complementation, Proceedings of the American Mathematical Society 51:176-178 (1975) (doi:10.1090/S0002-9939-1975-0373893-X)
N. D. Goodman J. Myhill, Choice Implies Excluded Middle, Zeitschrift fuer Mathematische Logik und Grundlagen der Mathematik 24:461 (1978)
Review includes
See also
Last revised on July 2, 2023 at 04:46:28. See the history of this page for a list of all contributions to it.